Reversible Computation in Term Rewriting111This work has been partially supported by the EU
(FEDER) and the Spanish Ministerio de Economía y
Competitividad (MINECO) under grants TIN2013-44742-C4-1-R and
TIN2016-76843-C4-1-R, by the Generalitat Valenciana under
grant PROMETEO-II/2015/013 (SmartLogic), and by the COST Action
IC1405 on Reversible Computation - extending
horizons of computing.
Adrián Palacios was partially supported by the EU (FEDER) and
the Spanish Ayudas para contratos predoctorales para la
formación de doctores and Ayudas a la movilidad
predoctoral para la realización de estancias breves en centros
de I+D, MINECO (SEIDI), under FPI grants BES-2014-069749 and
EEBB-I-16-11469.
Part of this research was done while the second and third authors
were visiting Nagoya University; they gratefully acknowledge their
hospitality.
© 2017. This manuscript version is made available under the
CC-BY-NC-ND 4.0 license
http://creativecommons.org/licenses/by-nc-nd/4.0/
Abstract
Essentially, in a reversible programming language, for each forward computation from state to state , there exists a constructive method to go backwards from state to state . Besides its theoretical interest, reversible computation is a fundamental concept which is relevant in many different areas like cellular automata, bidirectional program transformation, or quantum computing, to name a few.
In this work, we focus on term rewriting, a computation model that
underlies most rule-based programming languages. In general, term
rewriting is not reversible, even for injective functions; namely,
given a rewrite step , we do not always have a
decidable method to get from .
Here, we introduce a conservative extension of term rewriting that
becomes reversible.
Furthermore, we also define two transformations, injectivization
and inversion, to make a rewrite system reversible using standard
term rewriting. We illustrate the usefulness of our transformations
in the context of bidirectional program transformation.
To appear in the Journal of Logical and Algebraic Methods in Programming.
keywords:
term rewriting , reversible computation , program transformation1 Introduction
The notion of reversible computation can be traced back to Landauer’s pioneering work [22]. Although Landauer was mainly concerned with the energy consumption of erasing data in irreversible computing, he also claimed that every computer can be made reversible by saving the history of the computation. However, as Landauer himself pointed out, this would only postpone the problem of erasing the tape of a reversible Turing machine before it could be reused. Bennett [6] improved the original proposal so that the computation now ends with a tape that only contains the output of a computation and the initial source, thus deleting all remaining “garbage” data, though it performs twice the usual computation steps. More recently, Bennett’s result is extended in [9] to nondeterministic Turing machines, where it is also proved that transforming an irreversible Turing machine into a reversible one can be done with a quadratic loss of space. We refer the interested reader to, e.g., [7, 14, 40] for a high level account of the principles of reversible computation.
In the last decades, reversible computing and reversibilization (transforming an irreversible computation device into a reversible one) have been the subject of intense research, giving rise to successful applications in many different fields, e.g., cellular automata [28], where reversibility is an essential property, bidirectional program transformation [24], where reversibility helps to automate the generation of inverse functions (see Section 6), reversible debugging [17], where one can go both forward and backward when seeking the cause of an error, parallel discrete event simulation [34], where reversible computation is used to undo the effects of speculative computations made on a wrong assumption, quantum computing [39], where all computations should be reversible, and so forth. The interested reader can find detailed surveys in the state of the art reports of the different working groups of COST Action IC1405 on Reversible Computation [20].
In this work, we introduce reversibility in the context of term rewriting [4, 36], a computation model that underlies most rule-based programming languages. In contrast to other, more ad-hoc approaches, we consider that term rewriting is an excellent framework to rigorously define reversible computation in a functional context and formally prove its main properties. We expect our work to be useful in different (sequential) contexts, like reversible debugging, parallel discrete event simulation or bidirectional program transformation, to name a few. In particular, Section 6 presents a first approach to formalize bidirectional program transformation in our setting.
To be more precise, we present a general and intuitive notion of reversible term rewriting by defining a Landauer embedding. Given a rewrite system and its associated (standard) rewrite relation , we define a reversible extension of rewriting with two components: a forward relation and a backward relation , such that is a conservative extension of and, moreover, . We note that the inverse rewrite relation, , is not an appropriate basis for “reversible” rewriting since we aim at defining a technique to undo a particular reduction. In other words, given a rewriting reduction , our reversible relation aims at computing the term from and in a decidable and deterministic way, which is not possible using since it is generally non-deterministic, non-confluent, and non-terminating, even for systems defining injective functions (see Example 6). In contrast, our backward relation is deterministic (thus confluent) and terminating. Moreover, our relation proceeds backwards step by step, i.e., the number of reduction steps in and are the same.
In order to introduce a reversibilization transformation for rewrite systems, we use a flattening transformation so that the reduction at top positions of terms suffices to get a normal form in the transformed systems. For instance, given the following rewrite system:
defining the addition on natural numbers built from constructors and , we produce the following flattened (conditional) system:
(see Example 29 for more details). This allows us to provide an improved notion of reversible rewriting in which some information (namely, the positions where reduction takes place) is not required anymore. This opens the door to compile the reversible extension of rewriting into the system rules. Loosely speaking, given a system , we produce new systems and such that standard rewriting in , i.e., , coincides with the forward reversible extension in the original system, and analogously is equivalent to . E.g., for the system above, we would produce
where is an injective version of function , is the inverse of , and are fresh symbols introduced to label the rules of .
In this work, we will mostly consider conditional rewrite systems, not only to have a more general notion of reversible rewriting, but also to define a reversibilization technique for unconditional rewrite systems, since the application of flattening (cf. Section 4) may introduce conditions in a system that is originally unconditional, as illustrated above.
This paper is an extended version of [31]. In contrast to [31], our current paper includes the proofs of technical results, the reversible extension of term rewriting is introduced first in the unconditional case (which is simpler and more intuitive), and presents an improved injectivization transformation when the system includes injective functions. Furthermore, a prototype implementation of the reversibilization technique is publicly available from http://kaz.dsic.upv.es/rev-rewriting.html.
The paper is organized as follows. After introducing some preliminaries in Section 2, we present our approach to reversible term rewriting in Section 3. Section 4 introduces the class of pure constructor systems where all reductions take place at topmost positions, so that storing this information in reversible rewrite steps becomes unnecessary. Then, Section 5 presents injectivization and inversion transformations in order to make a rewrite system reversible with standard rewriting. Here, we also present an improvement of the transformation for injective functions. The usefulness of these transformations is illustrated in Section 6. Finally, Section 7 discusses some related work and Section 8 concludes and points out some ideas for future research.
2 Preliminaries
We assume familiarity with basic concepts of term rewriting. We refer the reader to, e.g., [4] and [36] for further details.
2.1 Terms and Substitutions
A signature is a set of ranked function symbols. Given a set of variables with , we denote the domain of terms by . We use to denote functions and to denote variables. Positions are used to address the nodes of a term viewed as a tree. A position in a term , in symbols , is represented by a finite sequence of natural numbers, where denotes the root position. We let denote the subterm of at position and the result of replacing the subterm by the term . denotes the set of variables appearing in . We also let denote . A term is ground if .
A substitution is a mapping from variables to terms such that is its domain. A substitution is ground if is ground for all . Substitutions are extended to morphisms from to in the natural way. We denote the application of a substitution to a term by rather than . The identity substitution is denoted by . We let “” denote the composition of substitutions, i.e., . The restriction of a substitution to a set of variables is defined as follows: if and otherwise.
2.2 Term Rewriting Systems
A set of rewrite rules such that is a nonvariable term and is a term whose variables appear in is called a term rewriting system (TRS for short); terms and are called the left-hand side and the right-hand side of the rule, respectively. We restrict ourselves to finite signatures and TRSs. Given a TRS over a signature , the defined symbols are the root symbols of the left-hand sides of the rules and the constructors are . Constructor terms of are terms over and , denoted by . We sometimes omit from and if it is clear from the context. A substitution is a constructor substitution (of ) if for all variables .
For a TRS , we define the associated rewrite relation as the smallest binary relation on terms satisfying the following: given terms , we have iff there exist a position in , a rewrite rule , and a substitution such that and ; the rewrite step is sometimes denoted by to make explicit the position and rule used in this step. The instantiated left-hand side is called a redex. A term is called irreducible or in normal form with respect to a TRS if there is no term with . A substitution is called normalized with respect to if every variable in the domain is replaced by a normal form with respect to . We sometimes omit “with respect to ” if it is clear from the context. A derivation is a (possibly empty) sequence of rewrite steps. Given a binary relation , we denote by its reflexive and transitive closure, i.e., means that can be reduced to in in zero or more steps; we also use to denote that can be reduced to in exactly steps.
We further assume that rewrite rules are labelled, i.e., given a TRS , we denote by a rewrite rule with label . Labels are unique in a TRS. Also, to relate label to fixed variables, we consider that the variables of the rewrite rules are not renamed222This will become useful in the next section where the reversible extension of rewriting keeps a “history” of a computation in the form of a list of terms , and we want the domain of to be a subset of the left-hand side of the rule labelled with . and that the reduced terms are always ground. Equivalently, one could require terms to be variable disjoint with the variables of the rewrite system, but we require groundness for simplicity. We often write instead of if rule is labeled with .
2.3 Conditional Term Rewrite Systems
In this paper, we also consider conditional term rewrite systems (CTRSs); namely oriented 3-CTRSs, i.e., CTRSs where extra variables are allowed as long as for any rule [26]. In oriented CTRSs, a conditional rule has the form , where each oriented equation is interpreted as reachability (). In the following, we denote by a sequence of elements for some . We also write for the sequence when (and the empty sequence otherwise). We write when the number of elements is not relevant. In addition, we denote a condition by .
As in the unconditional case, we consider that rules are labelled and that labels are unique in a CTRS. And, again, to relate label to fixed variables, we consider that the variables of the conditional rewrite rules are not renamed and that the reduced terms are always ground.
For a CTRS , the associated rewrite relation is defined as the smallest binary relation satisfying the following: given ground terms , we have iff there exist a position in , a rewrite rule , and a ground substitution such that , for all , and .
In order to simplify the presentation, we only consider deterministic CTRSs (DCTRSs), i.e., oriented 3-CTRSs where, for each rule , we have for all (see Section 3.2 for a justification of this requirement and how it could be relaxed to arbitrary 3-CTRSs). Intuitively speaking, the use of DCTRs allows us to compute the bindings for the variables in the condition of a rule in a deterministic way. E.g., given a ground term and a rule with , we have that is ground. Therefore, one can reduce to some term such that is an instance of with some ground substitution . Now, we have that is ground and we can reduce to some term such that is an instance of with some ground substitution , and so forth. If all equations in the condition hold using , we have that with .
Example 1
Consider the following DCTRS that defines the function that doubles the value of its argument when it is an even natural number:
Given the term we have, for instance, the following derivation:
3 Reversible Term Rewriting
In this section, we present a conservative extension of the rewrite relation which becomes reversible. In the following, we use to denote our reversible (forward) term rewrite relation, and to denote its application in the reverse (backward) direction. Note that, in principle, we do not require , i.e., we provide independent (constructive) definitions for each relation. Nonetheless, we will prove that indeed holds (cf. Theorems 9 and 20). In some approaches to reversible computing, both forward and backward relations should be deterministic. Here, we will only require deterministic backward steps, while forward steps might be non-deterministic, as it is often the case in term rewriting.
3.1 Unconditional Term Rewrite Systems
We start with unconditional TRSs since it is conceptually simpler and thus will help the reader to better understand the key ingredients of our approach. In the next section, we will consider the more general case of DCTRSs.
Given a TRS , reversible rewriting is defined on pairs , where is a ground term and is a trace (the “history” of the computation so far). Here, a trace in is a list of trace terms of the form such that is a label for some rule , is a position, and is a substitution with which will record the bindings of erased variables when (and if ).333Note that if a rule is non-erasing, i.e., , then . Our trace terms have some similarities with proof terms [36]. However, proof terms do not store the bindings of erased variables (and, to the best of our knowledge, they are only defined for unconditional TRSs, while we use trace terms both for unconditional and conditional TRSs).
Our reversible term rewriting relation is only defined on safe pairs:
Definition 2
Let be a TRS. The pair is safe in iff, for all in , is a ground substitution with and .
In the following, we often omit when referring to traces and safe pairs if the underlying TRS is clear from the context.
Safety is not necessary when applying a forward reduction step, but will become essential for the backward relation to be correct. E.g., all traces that come from the forward reduction of some initial pair with an empty trace will be safe (see below). Reversible rewriting is then introduced as follows:
Definition 3
Let be a TRS. A reversible rewrite relation is defined on safe pairs , where is a ground term and is a trace in . The reversible rewrite relation extends standard rewriting as follows:444In the following, we consider the usual infix notation for lists where is the empty list and is a list with head and tail .
iff there exist a position , a rewrite rule , and a ground substitution such that , , and . The reverse relation, , is then defined as follows:
iff is a safe pair in and there exist a ground substitution and a rule such that , and . Note that , where is the union of substitutions, since , and both substitutions are ground, so .
We denote the union of both relations by .
Example 4
Let us consider the following TRS defining the addition on natural numbers built from and , and the function that returns its first argument:
Given the term , we have, for instance, the following reversible (forward) derivation:
The reader can easily check that is reducible to using the backward relation by performing exactly the same steps but in the backward direction.
An easy but essential property of is that it is a conservative extension of standard rewriting in the following sense (we omit its proof since it is straightforward):
Theorem 5
Let be a TRS. Given terms , if , then for any trace there exists a trace such that .
Here, and in the following, we assume that , i.e., is denoted by . Observe that the backward relation is not a conservative extension of : in general, does not imply for any arbitrary trace . This is actually the purpose of our notion of reversible rewriting: should not extend but is only aimed at performing exactly the same steps of the forward computation whose trace was stored, but in the reverse order. Nevertheless, one can still ensure that for all steps , there exists some trace such that (which is an easy consequence of the above result and Theorem 9 below).
Example 6
Consider again the following TRS . Given the reduction , there are infinitely many reductions for using , e.g., , , , etc. The relation is also non-terminating: . In contrast, given a pair , we can only perform a single deterministic and finite reduction (as proved below). For instance, if , then the only possible reduction is .
Now, we state a lemma which shows that safe pairs are preserved through reversible term rewriting (both in the forward and backward directions):
Lemma 7
Let be a TRS. Let be a safe pair. If , then is also safe.
Proof 1
We prove the claim by induction on the length of the derivation. Since the base case is trivial, consider the inductive case . Assume a derivation of the form . By the induction hypothesis, we have that is a safe pair. Now, we distinguish two cases depending on the last step. If we have , then there exist a position , a rewrite rule , and a ground substitution such that , , , and . Then, since is ground and by construction, the claim follows straightforwardly. If the last step has the form , then the claim follows trivially since each step with only removes trace terms from . \qed
Hence, since any pair with an empty trace is safe the following result, which states that every pair that is reachable from an initial pair with an empty trace is safe, straightforwardly follows from Lemma 7:
Proposition 8
Let be a TRS. If , then is safe.
Now, we state the reversibility of , i.e., the fact that (and thus the reversibility of and , too).
Theorem 9
Let be a TRS. Given the safe pairs and , for all , iff .
Proof 2
We prove the claim by induction on the length of the derivation . Since the base case is trivial, let us consider the inductive case . Consider a derivation . By Lemma 7, both and are safe. By the induction hypothesis, we have . Consider now the step . Then, there is a position , a rule and a ground substitution such that , , , and . Let . Then, we have with , and . Moreover, since , we have , and the claim follows.
This direction proceeds in a similar way. We prove the claim by induction on the length of the derivation . As before, we only consider the inductive case . Let us consider a derivation . By Lemma 7, both and are safe. By the induction hypothesis, we have . Consider now the reduction step . Then, we have , , and there exists a ground substitution with such that and . Moreover, since is safe, we have that and, thus, . Let . Then, since and , we can perform the step with , and the claim follows. \qed
The next corollary is then immediate:
Corollary 10
Let be a TRS. Given the safe pairs and , for all , iff .
A key issue of our notion of reversible rewriting is that the backward rewrite relation is deterministic (thus confluent), terminating, and has a constructive definition:
Theorem 11
Let be a TRS. Given a safe pair , there exists at most one pair such that .
Proof 3
First, if there is no step using from , the claim follows trivially. Now, assume there is at least one step . We prove that this is the only possible step. By definition, we have , , , and there exists a ground substitution with such that and . The only source of nondeterminism may come from choosing a rule labeled with and from the computation of the substitution . The claim follows trivially from the fact that labels are unique in and that, if there is some ground substitution with and , then . \qed
Therefore, is clearly deterministic and confluent. Termination holds straightforwardly for pairs with finite traces since its length strictly decreases with every backward step. Note however that even when and are terminating, the relation is always non-terminating since one can keep going back and forth.
3.2 Conditional Term Rewrite Systems
In this section, we extend the previous notions and results to DCTRSs. We note that considering DCTRSs is not enough to make conditional rewriting deterministic. In general, given a rewrite step with a position of , a rule, and a substitution such that and for all , there are three potential sources of non-determinism: the selected position , the selected rule , and the substitution . The use of DCTRSs can only make deterministic the last one, but the choice of a position and the selection of a rule may still be non-deterministic.
For DCTRSs, the notion of a trace term used for TRSs is not sufficient since we also need to store the traces of the subderivations associated to the condition of the applied rule (if any). Therefore, we generalize the notion of a trace as follows:
Definition 12 (trace)
Given a CTRS , a trace in is recursively defined as follows:
-
1.
the empty list is a trace;
-
2.
if are traces in , , is a rule, is a position, and is a ground substitution, then is a trace in .
We refer to each component in a trace as a trace term.
Intuitively speaking, a trace term stores the position of a reduction step, a substitution with the bindings that are required for the step to be reversible (e.g., the bindings for the erased variables, but not only; see below) and the traces associated to the subcomputations in the condition.
The notion of a safe pair is now more involved in order to deal with conditional rules. The motivation for this definition will be explained below, after introducing reversible rewriting for DCTRSs.
Definition 13 (safe pair)
Let be a DCTRS. A trace is safe in iff, for all trace terms in , is a ground substitution with , , and are safe too. The pair is safe in iff is safe.
Reversible (conditional) rewriting can now be introduced as follows:
Definition 14 (reversible rewriting)
Let be a DCTRS. The reversible rewrite relation is defined on safe pairs , where is a ground term and is a trace in . The reversible rewrite relation extends standard conditional rewriting as follows:
iff there exist a position , a rewrite rule , and a ground substitution such that , for all , , and . The reverse relation, , is then defined as follows:
iff is a safe pair in , and there is a ground substitution such that , , for all , and . Note that since and both substitutions are ground.
As in the unconditional case, we denote the union of both relations by .
Example 15
Consider again the DCTRS from Example 1:
Given the term , we have, for instance, the following forward derivation:
where since we have the following reduction:
The reader can easily construct the associated backward derivation:
Let us now explain why we need to store in a step of the form . Given a DCTRS, for each rule , the following conditions hold:
-
1.
3-CTRS: .
-
2.
Determinism: for all , we have .
Intuitively, the backward relation can be seen as equivalent to the forward relation but using a reverse rule of the form . Therefore, in order to ensure that backward reduction is deterministic, we need the same conditions as above but on the reverse rule:555We note that the notion of a non-erasing rule is extended to the DCTRSs in [32], which results in a similar condition.
-
1.
3-CTRS: .
-
2.
Determinism: for all , .
Since these conditions cannot be guaranteed in general, we store
in the trace term so that is deterministic and fulfills the conditions of a 3-CTRS by construction, i.e., and for all , ; see the proof of Theorem 21 for more details.
Example 16
Consider the following DCTRS:
and the step with , and . The binding of variable is required to recover the value of the erased variable , but the binding of variable is also needed to perform the subderivation when applying a backward step from . If the binding for were unknown, this step would not be deterministic. As mentioned above, an instantiated reverse rule would be a legal DCTRS rule thanks to .
We note that similar conditions could be defined for arbitrary 3-CTRSs. However, the conditions would be much more involved; e.g., one had to compute first the variable dependencies between the equations in the conditions. Therefore, we prefer to keep the simpler conditions for DCTRSs (where these dependencies are fixed), which is still quite a general class of CTRSs.
Reversible rewriting is also a conservative extension of rewriting for DCTRSs (we omit the proof since it is straightforward):
Theorem 17
Let be a DCTRS. Given ground terms , if , then for any trace there exists a trace such that .
For the following result, we need some preliminary notions (see, e.g., [36]). For every oriented CTRS , we inductively define the TRSs , , as follows:
Observe that for all . We have . We also have iff for some . The minimum such is called the depth of , and the maximum depth of (i.e., is the maximum of depths ) is called the depth of the derivation. If a derivation has depth and length , we write . Analogous notions can naturally be defined for , , and .
The next result shows that safe pairs are also preserved through reversible rewriting with DCTRSs:
Lemma 18
Let be a DCTRS and a safe pair. If , then is also safe.
Proof 4
We prove the claim by induction on the lexicographic product of the depth and the length of the derivation . Since the base case is trivial, we consider the inductive case . Consider a derivation . By the induction hypothesis, we have that is safe. Now, we distinguish two cases depending on the last step. If the last step is , then there exist a position , a rewrite rule , and a ground substitution such that , for all , , , and . Then, since , , is ground and by construction, the claim follows by induction. Finally, if the last step has the form , then the claim follows trivially since a step with only removes trace terms from . \qed
As in the unconditional case, the following proposition follows straightforwardly from the previous lemma since any pair with an empty trace is safe.
Proposition 19
Let be a DCTRS. If , then is safe in .
Now, we can already state the reversibility of for DCTRSs:
Theorem 20
Let be a DCTRS. Given the safe pairs and , for all , iff .
Proof 5
We prove the claim by induction on the lexicographic product of the depth and the length of the derivation . Since the base case is trivial, we consider the inductive case . Consider a derivation whose associated product is . By Proposition 19, both and are safe. By the induction hypothesis, since , we have . Consider now the step . Thus, there exist a position , a rule , and a ground substitution such that , for all , , , and . By definition of , we have that and, thus, for all and for all . Hence, by the induction hypothesis, we have for all . Let , so that and . Therefore, we have with , and , and the claim follows.
This direction proceeds in a similar way. We prove the claim by induction on the lexicographic product of the depth and the length of the considered derivation. Since the base case is trivial, let us consider the inductive case . Consider a derivation whose associated product is . By Proposition 19, both and are safe. By the induction hypothesis, since , we have . Consider now the step . Then, we have , , and there exists a ground substitution with such that , for all , and . Moreover, since is safe, we have that . By definition of , we have that and, thus, for all and for all . By the induction hypothesis, we have for all . Let , with . Then, since , we can perform the step with ; moreover, since , which concludes the proof. \qed
In the following, we say that is a deterministic step if there is no other, different pair with and, moreover, the subderivations for the equations in the condition of the applied rule (if any) are deterministic, too. We say that a derivation is deterministic if each reduction step in the derivation is deterministic.
Now, we can already prove that backward reversible rewriting is also deterministic, as in the unconditional case:
Theorem 21
Let be a DCTRS. Let be a safe pair with for some term and trace . Then is deterministic.
Proof 6
We prove the claim by induction on the lexicographic product of the depth and the length of the steps. The case is trivial, and thus we let . Assume . For the base case , the applied rule is unconditional and the proof is analogous to that of Theorem 11.
Let us now consider . By definition, if , we have , and there exists a ground substitution with such that , , , for all , and . By the induction hypothesis, the subderivations are deterministic, i.e., is a unique resulting term obtained by reducing . Therefore, the only remaining source of nondeterminism can come from choosing a rule labeled with and from the computed substitution . On the one hand, the labels are unique in . As for , we prove that this is indeed the only possible substitution for the reduction step. Consider the instance of rule with : . Since is safe, we have that is a ground substitution and . Then, the following properties hold:
-
1.
, since is ground and it covers all the variables in .
-
2.
for all , since is ground and it covers all variables in .
The above properties guarantee that a rule of the form can be seen as a rule of a DCTRS and, thus, there exists a deterministic procedure to compute , which completes the proof. \qed
Therefore, is deterministic and confluent. Termination is trivially guaranteed for pairs with a finite trace since the trace’s length strictly decreases with every backward step.
4 Removing Positions from Traces
Once we have a feasible definition of reversible rewriting, there are two refinements that can be considered: i) reducing the size of the traces and ii) defining a reversibilization transformation so that standard rewriting becomes reversible in the transformed system. In this section, we consider the first problem, leaving the second one for the next section.
In principle, one could remove information from the traces by requiring certain conditions on the considered systems. For instance, requiring injective functions may help to remove rule labels from trace terms. Also, requiring non-erasing rules may help to remove the second component of trace terms (i.e., the substitutions). In this section, however, we deal with a more challenging topic: removing positions from traces. This is useful not only to reduce the size of the traces but it is also essential to define a reversibilization technique for DCTRSs in the next section.666We note that defining a transformation with traces that include positions would be a rather difficult task because positions are dynamic (i.e., they depend on the term being reduced) and thus would require a complex (and inefficient) system instrumentation. In particular, we aim at transforming a given DCTRS into one that fulfills some conditions that make storing positions unnecessary.
In the following, given a CTRS , we say that a term is basic [18] if it has the form with a defined function symbol and constructor terms. Furthermore, in the remainder of this paper, we assume that the right-hand sides of the equations in the conditions of the rules of a DCTRS are constructor terms. This is not a significant restriction since these terms cannot be reduced anyway (since we consider oriented equations in this paper), and still covers most practical examples.
Now, we introduce the following subclass of DCTRSs:
Definition 22 (pcDCTRS [30])
We say that a DCTRS is a pcDCTRS (“pc” stands for pure constructor) if, for each rule , we have that and are basic terms and and are constructor terms.
Pure constructor systems are called normalized systems in [3]. Also, they are mostly equivalent to the class IIIn of conditional systems in [8], where are required to be ground unconditional normal forms instead.777Given a CTRS , we define . A term is an unconditional normal form in , if it is a normal form in .
In principle, any DCTRS with basic terms in the left-hand sides (i.e., a constructor DCTRS) and constructor terms in the right-hand sides of the equations of the rules can be transformed into a pcDCTRS by applying a few simple transformations: flattening and simplification of constructor conditions. Let us now consider each of these transformations separately. Roughly speaking, flattening involves transforming a term (occurring, e.g., in the right-hand side of a DCTRS or in the condition) with nested defined functions like into a term and an (oriented) equation , where is a fresh variable. Formally,
Definition 23 (flattening)
Let be a CTRS, be a rule and be a new rule either of the form , for some , , or , for some , where is a fresh variable.888The positions can be required to be different from , but this is not strictly necessary. Then, a CTRS is obtained from by a flattening step if .
Note that, if an unconditional rule is non-erasing (i.e., for a rule ), any conditional rule obtained by flattening is trivially non-erasing too, according to the notion of non-erasingness for DCTRSs in [32].999Roughly, a DCTRS is considered non-erasing in [32] if its transformation into an unconditional TRS by an unraveling transformation gives rise to a non-erasing TRS.
Flattening is trivially complete since any flattening step can be undone by binding the fresh variable again to the selected subterm and, then, proceeding as in the original system. Soundness is more subtle though. In this work, we prove the correctness of flattening for arbitrary DCTRSs with respect to innermost rewriting. As usual, the innermost rewrite relation, in symbols, , is defined as the smallest binary relation satisfying the following: given ground terms , we have iff there exist a position in such that no proper subterms of are reducible, a rewrite rule , and a normalized ground substitution such that , , for all , and .
In order to prove the correctness of flattening, we state the following auxiliary lemma:
Lemma 24
Let be a DCTRS. Given terms and , with a normal form, and a position , we have iff and , for some fresh variable and normalized substitution .
Proof 7
Let us consider an arbitrary position . If is normalized, the proof is straightforward. Otherwise, since we use innermost reduction (leftmost innermost, for simplicity), we can represent the derivation as follows:
where is a normal form and the subderivation reduces the leftmost innermost subterms that are to the left of (if any). Then, by choosing we have (by mimicking the steps of ), (by mimicking the steps of ), and (by mimicking the steps of ), which concludes the proof.
This direction is perfectly analogous to the previous case. We consider an arbitrary position such that is not normalized (otherwise, the proof is trivial). Now, since derivations are innermost, we can consider that is as follows: , where reduces the innermost subterms to the left of . Therefore, we have (by mimicking the steps of ), (by mimicking the steps of , with ), and (by mimicking the steps of ). \qed
The following theorem is an easy consequence of the previous lemma:
Theorem 25
Let be a DCTRS. If is obtained from by a flattening step, then is a DCTRS and, for all ground terms , with a normal form, we have iff .
Proof 8
We prove the claim by induction on the lexicographic product of the depth and the length of the derivation . Since the base case is trivial, we consider the inductive case . Assume that has the form with and , , . If , the claim follows directly by induction. Otherwise, we have that either , for some , , or , for some , where is a fresh variable. Consider first the case , for some , . Since , , , by the induction hypothesis, we have , . By Lemma 24, there exists for some normal form such that and . Moreover, since is an extra variable, we also have for . Therefore, since and , we have , and the claim follows by induction. Consider the second case. By the induction hypothesis, we have and for all . By Lemma 24, there exists a substitution such that is the normal form of and we have and . Moreover, since is a fresh variable, we have for all . Therefore, we have , which concludes the proof.
This direction is perfectly analogous to the previous one, and follows easily by Lemma 24 too. \qed
Let us now consider the second kind of transformations: the simplification of constructor conditions. Basically, we can drop an equation when the terms and are constructor, called a constructor condition, by either applying the most general unifier (mgu) of and (if it exists) to the remaining part of the rule, or by deleting entirely the rule if they do not unify because (under innermost rewriting) the equation will never be satisfied by any normalized substitution. Similar transformations can be found in [33].
In order to justify these transformations, we state and prove the following results. In the following, we let denote the most general unifier of terms and if it exists, and otherwise.
Theorem 26 (removal of unifiable constructor conditions)
Let be a DCTRS and let be a rule with , for some , where and are constructor terms. Let be a new rule of the form .101010In [33], the condition is required, but this condition is not really necessary. Then is a DCTRS and, for all ground terms and , we have iff .
Proof 9
First, we prove the following claim by induction on the lexicographic product of the depth and the length of the steps: if , then . It suffices to consider the case where is applied, i.e., with for all . By definition, is normalized. Hence, since and are constructor terms, we have that and are trivially normal forms since the normalized subterms introduced by cannot become reducible in a constructor context. Therefore, we have . Thus, is a unifier of and and, hence, is more general than . Let be a substitution such that . Since is normalized, so is . Since for all , by the induction hypothesis, we have that for . Therefore, we have that .
Now, we prove the following claim by induction on the lexicographic product of the depth and the length of the steps: if , then . It suffices to consider the case where is applied, i.e., with for all . By the assumption and the definition, and are normalized, and thus, and are normal forms (as in the previous case, because the normalized subterms introduced by cannot become reducible in a constructor context), i.e., . Since for all , by the induction hypothesis, we have that for . Therefore, we have that with . \qed
Now we consider the case when the terms in the constructor condition do not unify:
Theorem 27 (removal of infeasible rules)
Let be a DCTRS and let be a rule with , for some . Then is a DCTRS and, for all ground terms and , we have iff .
Proof 10
Since , the if part is trivial, and thus, we consider the only-if part. To apply to a term, there must exist a normalized substitution such that . Since are constructor terms and is normalized, is a normal form (because the normalized subterms introduced by cannot become reducible in a constructor context). If is satisfied (i.e., ), then and are unifiable, and thus, this contradicts the assumption. Therefore, is never applied to any term, and hence, iff . \qed
Using flattening and the simplification of constructor conditions, any constructor DCTRS with constructor terms in the right-hand sides of the equations of the rules can be transformed into a pcDCTRS. One can use, for instance, the following simple algorithm. Let be such a constructor DCTRS. We apply the following transformations as much as possible:
- (flattening-rhs)
-
Assume that contains a rule of the form where is not a constructor term. Let , , be a basic subterm of . Then, we replace rule by a new rule of the form , where is a fresh variable.
- (flattening-condition)
-
Assume that contains a rule of the form where is neither a constructor term nor a basic term, . Let , , be a basic subterm of . Then, we replace rule by a new rule of the form , where is a fresh variable.
- (removal-unify)
-
Assume that contains a rule of the form where is a constructor term, . If , then we replace rule by a new rule of the form .
- (removal-fail)
-
Assume that contains a rule of the form where is a constructor term, . If , then we remove rule from .
Trivially, by applying rule flattening-rhs as much as possible, we end up with a DCTRS where all the right-hand sides are constructor terms; analogously, the exhaustive application of rule flattening-condition allows us to ensure that the left-hand sides of all equations in the conditions of the rules are either constructor or basic; finally, the application of rules removal-unify and removal-fail produces a pcDCTRS by removing those equations in which the left-hand side is a constructor term. Therefore, in the remainder of this paper, we only consider pcDCTRSs.
A nice property of pcDCTRSs is that one can consider reductions only at topmost positions. Formally, given a pcDCTRS , we say that is a top reduction step if , there is a ground substitution with , for all , , and all the steps in for are also top reduction steps. We denote top reductions with for standard rewriting, and for our reversible rewrite relations.
The following result basically states that and are equivalent for pcDCTRSs:
Theorem 28
Let be a constructor DCTRS with constructor terms in the right-hand sides of the equations and be a pcDCTRS obtained from by a sequence of transformations of flattening and simplification of constructor conditions. Given ground terms and such that is basic and is normalized, we have iff .
Proof 11
First, it is straightforward to see that an innermost reduction in can only reduce the topmost positions of terms since defined functions can only occur at the root of terms and the terms introduced by instantiation are, by definition, irreducible. Therefore, the claim is a consequence of Theorems 25, 26 and 27, together with the above fact. \qed
Therefore, when considering pcDCTRSs and top reductions, storing the reduced positions in the trace terms becomes redundant since they are always . Thus, in practice, one can consider simpler trace terms without positions, , that implicitly represent the trace term .
Example 29
Consider the following TRS defining addition and multiplication on natural numbers, and its associated pcDCTRS :
For instance, given the following reduction in :
we have the following counterpart in :
Trivially, all results in Section 3 hold for pcDCTRSs and top reductions starting from basic terms. The simpler trace terms without positions will allow us to introduce appropriate injectivization and inversion transformations in the next section.
5 Reversibilization
In this section, we aim at compiling the reversible extension of rewriting into the system rules. Intuitively speaking, given a pure constructor system , we aim at producing new systems and such that standard rewriting in , i.e., , coincides with the forward reversible extension in the original system, and analogously is equivalent to . Therefore, can be seen as an injectivization of , and as the inversion of .
In principle, we could easily introduce a transformation for pcDCTRSs that mimicks the behavior of the reversible extension of rewriting. For instance, given the pcDCTRS of Example 16, we could produce the following injectivized version :111111We will write just instead of when no argument is required.
For instance, the reversible step with , and , has the following counterpart in :
The only subtle difference here is that a trace term like
is now stored in the transformed system as
Furthermore, we could produce an inverse of the above system as follows:
mainly by switching the left- and right-hand sides of each rule and condition. The correctness of these injectivization and inversion transformations would be straightforward.
These transformations are only aimed at mimicking, step by step, the reversible relations and . Roughly speaking, for each step in a system , we have , where is the injectivized version of , and for each step in , we have , where is the inverse of . More details on this approach can be found in [31]. Unfortunately, it might be much more useful to produce injective and inverse versions of each function defined in a system . Note that, in the above approach, the system only defines a single function and only defines , i.e., we are computing systems that define the relations and rather than the injectivized and inverse versions of the functions in . In the following, we introduce more refined transformations that can actually produce injective and inverse versions of the original functions.
5.1 Injectivization
In principle, given a function , one can consider that the injectivization of a rule of the form121212By abuse of notation, here we let denote sequences of terms of arbitrary length, i.e., , , etc.
produces the following rule
where and are fresh variables. The following example, though, illustrates that this is not correct in general.
Example 30
Consider the following pcDCTRS :
together with the following top reduction:
Following the scheme above, we would produce the following pcDCTRS
Unfortunately, the corresponding reduction for above cannot be done in this system since cannot be reduced to .
In order to overcome this drawback, one could complete the function definitions with rules that reduce each irreducible term to a tuple of the form . Although we find it a promising idea for future work, in this paper we propose a simpler approach. In the following, we consider a refinement of innermost reduction where only constructor substitutions are computed. Formally, the constructor reduction relation, , is defined as follows: given ground terms , we have iff there exist a position in such that no proper subterms of are reducible, a rewrite rule , and a ground constructor substitution such that , for all , and . Note that the results in the previous section also hold for .
In the following, given a basic term , we denote by the term . Now, we introduce our injectivization transformation as follows:
Definition 31 (injectivization)
Let be a pcDCTRS. We produce a new CTRS by replacing each rule of by a new rule of the form
in , where and are fresh variables. Here, we assume that the variables of are in lexicographic order.
Observe that now we do not need to keep a trace in each term, but only a single trace term since all reductions finish in one step in a pcDCTRS. The relation between the original trace terms and the information stored in the injectivized system is formalized as follows:
Definition 32
Given a trace term , we define recursively as follows: , where we assume that the variables are in lexicographic order.
Moreover, in order to simplify the notation, we consider that a a trace term and a singleton list of the form denote the same object. The correctness of the injectivization transformation is stated as follows:
Theorem 33
Let be a pcDCTRS and be its injectivization. Then is a pcDCTRS and, given a basic ground term , we have iff .
Proof 12
The fact that is a pcDCTRS is trivial. Regarding the second part, we proceed as follows:
We proceed by induction on the depth of the step . Since the depth is trivial, we consider the inductive case . Thus, there is a rule , and a substitution such that , , , , , and . By definition of , we have that for all and, thus, by the induction hypothesis, we have for all . Consider now the equivalent rule in : . Therefore, we have where and, thus, we can conclude that .
This direction is analogous. We proceed by induction on the depth of the step . Since the depth is trivial, we consider the inductive case . Thus, there is a rule in and a substitution such that , , , and . Assume that is the restriction of to the variables of the rule, excluding the fresh variables , and that for all . Therefore, and , . Then, by definition of , we have that for all and, thus, by the induction hypothesis, we have , . Consider now the equivalent rule in : . Therefore, we have , , and . Finally, since , we can conclude that . \qed
5.2 Inversion
Given an injectivized system, inversion basically amounts to switching the left- and right-hand sides of the rule and of every equation in the condition, as follows:
Definition 34 (inversion)
Let be a pcDCTRS and be its injectivization. The inverse system is obtained from by replacing each rule131313Here, we assume that , ,…, denote arbitrary sequences of terms, i.e., , , etc. We use this notation for clarity.
of by a new rule of the form
in , where the variables of are in lexicographic order.
Example 35
Consider again the pcDCTRS of Example 16. Here, injectivization returns the following pcDCTRS :
Then, inversion with produces the following pcDCTRS :
Finally, the correctness of the inversion transformation is stated as follows:
Theorem 36
Let be a pcDCTRS, its injectivization, and the inversion of . Then, is a basic pcDCTRS and, given a basic ground term and a constructor ground term with a safe pair, we have iff .
Proof 13
The fact that is a pcDCTRS is trivial. Regarding the second part, we proceed as follows.
We proceed by induction on the depth of the step . Since the depth is trivial, we consider the inductive case . Let . Thus, we have that is a safe pair, there is a rule and substitution with such that , for all , and . Note that denote sequences of terms of arbitrary length, i.e., , , etc. Since is a safe pair, we have that . By definition of , we have that for all and, by the induction hypothesis, we have for all . Let us now consider the equivalent rule in :
Hence, we have , where
and, thus, we can conclude that .
This direction is analogous. We proceed by induction on the depth of the step . Since the depth is trivial, we consider the inductive case . Thus, there is a rule in and a substitution such that , , , and . Assume that is the restriction of to the variables of the rule, excluding the fresh variables , and that for all . Therefore, , and , . Then, by definition of , we have that for all and, thus, by the induction hypothesis, we have , . Consider now the equivalent rule in : in . Therefore, we have ,
and . Finally, since , we can conclude that . \qed
5.3 Improving the transformation for injective functions
When a function is injective, one can expect the injectivization transformation to be unnecessary. This is not generally true, since some additional syntactic conditions might also be required. Furthermore, depending on the considered setting, it can be necessary to have an injective system, rather than an injective function. Consider, e.g., the following simple TRS:
Here, all functions are clearly injective. However, given a reduction like , we do not know which rule should be applied to in order to go backwards until the initial term (actually, both the second and the fourth rules are applicable in the reverse direction).
Luckily, in our context, the injectivity of a function suffices since reductions in pcDCTRSs are performed in a single step. Therefore, given a reduction of the form , a backward computation will have the form , so that we know that only the inverse rules of are applicable.
Now, we present an improvement of the injectivization transformation presented in Section 5.1 which has some similarities with that in [24]. Here, we consider that the initial system is a TRS since, to the best of our knowledge, there is no reachability analysis defined for DCTRSs. In the following, given a term , we let
i.e., returns a set with the constructor normal forms of all possible ground constructor instances of . Although computing this set is generally undecidable, there are some overapproximations based on the use of tree automata (see, e.g., [15] and the most recent approach for innermost rewriting [16]). Let us consider that is such an approximation, with for all terms . Here, we are interested in determining when the right-hand sides, and , of two rules do not overlap, i.e., . For this purpose, we will check whether . Since finite tree automata are closed under intersection and the emptiness of a finite tree automata is decidable, checking the emptiness of is decidable and can be used to safely identify non-overlapping right-hand sides, i.e., if , then and are definitely non-overlapping; otherwise, they may be overlapping or non-overlapping.
Now, we summarize our method to simplify some trace terms. Given a constructor TRS and a rule , we check the following conditions:
-
1.
the right-hand side of the rule does not overlap with the right-hand side of any other rule defining the same function;
-
2.
the rule is non-erasing, i.e., ;
-
3.
the right-hand side contains a single occurrence of a defined function symbol, say .
If these conditions hold, then the rule has the form with and basic terms,141414Note that is a basic term since we initially consider a constructor TRS and, thus, all left-hand sides are basic terms by definition. and and constructor terms, where is a fresh variable. In this case, we can safely produce the following injective version:151515Since is non-erasing, the pcDCTRS rule is trivially non-erasing too (according to [32], i.e., ) and, thus, no binding should be stored during the injectivization process.
instead of
Let us illustrate this improved transformation with a couple of examples.
Example 37
Consider the following TRS:
Here, it can easily be shown that , the two rules defining are non-erasing, and both contain a single occurrence of a defined function symbol in the righ-hand sides. Therefore, our improved injectivization applies and we get the following pcDCTRS :
In contrast, the original injectivization transformation would return the following system:
Finally, the inverse system obtained from using the original transformation has the following form:
For instance, given the forward reduction , we can build the corresponding backward reduction: .
Note, however, that the left-hand sides of overlap and we should reduce the conditions in order to determine which rule to apply. Therefore, in some cases, there is a trade-off between the size of the trace terms and the complexity of the reduction steps.
The example above, though, only produces a rather limited improvement since the considered functions are not recursive. Our next example shows a much significant improvement. Here, we consider the function (also used in [24] to illustrate the benefits of an injectivity analysis).
Example 38
Consider the following TRS defining the function :
Here, since the third rule is non-erasing, its right-hand side contains a single occurrence of a defined function, , and it does not overlap with any other right-hand side, our improved injectivization applies and we get the following pcDCTRS :
In contrast, the original injectivization transformation would return the following system :
It might seem a small difference, but if we call with two lists of elements, the system would build a trace term of the form with nested constructors , while would just build the trace term . For large values of , this is a significant improvement in memory usage.
6 Bidirectional Program Transformation
We illustrate a practical application of our reversibilization technique in the context of bidirectional program transformation (see [10] for a survey). In particular, we consider the so-called view-update problem. Here, we have a data structure (e.g., a database) called the source, which is transformed to another data structure, called the view. Typically, we have a view function, that takes the source and returns the corresponding view, together with an update function, that propagates the changes in a modified view to the original source. Two basic properties that these functions should satisfy in order to be well-behaved are the following [13]:
Bidirectionalization (first proposed in the database community [5]) basically consists in, given a view function, “bidirectionalize” it in order to derive an appropriate update function. For this purpose, first, a view complement function is usually defined, say , so that the tupled function
becomes injective. Therefore, the update function can be defined as follows:
This approach has been applied to bidirectionalize view functions in a functional language in [24].
In the following, we apply our injectivization and inversion transformations in order to produce a bidirectionalization transformation that may be useful in the context of the view-update problem (with some limitations). Let us assume that we have a view function, , that takes a source and returns the corresponding view, and which is defined by means of a pcDCTRS. Following our approach, given the original program , we produce an injectivized version and the corresponding inverse . Therefore, in principle, one can use , which will include the functions and , to define an update function as follows:
where is the original source, is the updated view, and , the returned value, is the corresponding updated source. Note that, in our context, the function is somehow equivalent to above.
Let us now illustrate the bidirectionalization process with an example. Consider a particular data structure, a list of records of the form where is the type of the record (e.g., , , , etc.) and is its price tag. The following system defines a view function that takes a type and a list of records, and returns a list with the price tags of the records of the given type:161616For simplicity, we restrict the record types to only and .
However, this system is not a pcDCTRS. Here, we use a flattening transformation to produce the following (labeled) pcDCTRS which is equivalent for constructor derivations:
Now, we can apply our injectivization transformation which returns the following pcDCTRS :
Finally, inversion returns the following pcDCTRS :
For instance, the term , reduces to in the original system . Given a modified view, e.g., , we can compute the modified source using function above:
Here, we have the following subcomputations:171717Note that, in this case, the function requires not only the source but also the additional parameter .
Thus returns the updated source , as expected. We note that the considered example cannot be transformed using the technique in [24], the closer to our approach, since the right-hand sides of some rules contain functions which are not treeless.181818A call is treeless if it has the form and are different variables. Nevertheless, one could consider a transformation from pcDCTRS to functional programs with treeless functions so that the technique in [24] becomes applicable.
Our approach can solve a view-update problem as long as the view function can be encoded in a pcDCTRS. When this is the case, the results from Section 5 guarantee that function is well defined. Formally analyzing the class of view functions that can be represented with a pcDCTRS is an interesting topic for further research.
7 Related Work
There is no widely accepted notion of reversible computing. In this work, we have considered one of its most popular definitions, according to which a computation principle is reversible if there is a method to undo a (forward) computation. Moreover, we expect to get back to an exact past state of the computation. This is often referred to as full reversibility.
As we have mentioned in the introduction, some of the most promising applications of reversibility include cellular automata [28], bidirectional program transformation [24], already discussed in Section 6, reversible debugging [17], where the ability to go both forward and backward when seeking the cause of an error can be very useful for the programmer, parallel discrete event simulation [34], where reversibility is used to undo the effects of speculative computations made on a wrong assumption, quantum computing [39], where all computations should be reversible, and so forth. The interested reader can find detailed surveys in the state of the art reports of the different working groups of COST Action IC1405 on Reversible Computation [20].
Intuitively speaking, there are two broad approaches to reversibility from a programming language perspective:
- Reversible programming languages.
- Irreversible programming languages and Landauer’s embedding.
-
Alternatively, one can consider an irreversible programming language, and enhance the states with some additional information (typically, the history of the computation so far) so that computations become reversible. This is called Landauer’s embedding.
In this work, we consider reversibility in the context of term rewriting. To the best of our knowledge, we have presented the first approach to reversibility in term rewriting. A closest approach was introduced by Abramsky in the context of pattern matching automata [2], though his developments could easily be applied to rewrite systems as well. In Abramsky’s approach, biorthogonality was required to ensure reversibility, which would be a very significant restriction for term rewriting systems. Basically, biorthogonality requires that, for every pair of (different) rewrite rules and , and do not overlap (roughly, they do not unify) and and do not overlap too. Trivially, the functions of a biorthogonal system are injective and, thus, computations are reversible without the need of a Landauer embedding. Therefore, Abramsky’s work is aimed at defining a reversible language, in contrast to our approach that is based on defining a Landauer embedding for standard term rewriting and a general class of rewrite systems.
Defining a Landauer embedding in order to make a computation mechanism reversible has been applied in different contexts and computational models, e.g., a probabilistic guarded command language [44], a low level virtual machine [35], the call-by-name lambda calculus [19, 21], cellular automata [38, 27], combinatory logic [11], a flowchart language [41], etc.
In the context of declarative languages, we find the work by Mu et al. [29], where a relational reversible language is presented (in the context of bidirectional programming). A similar approach was then introduced by Matsuda et al. [24, 25] in the context of functional programs and bidirectional transformation. The functional programs considered in [24] can be seen as linear and right-treeless191919There are no nested defined symbols in the right-hand sides, and, moreover, any term rooted by a defined function in the right-hand sides can only take different variables as its proper subterms. constructor TRSs. The class of functional programs is more general in [25], which would correspond to left-linear, right-treeless TRSs. The reversibilization technique of [24, 25] includes both an injectivization stage (by introducing a view complement function) and an inversion stage. These methods are closely related to the transformations of injectivization and inversion that we have presented in Section 5, although we developed them from a rather different starting point. Moreover, their methods for injectivization and inversion consider a more restricted class of systems than those considered in this paper. On the other hand, they apply a number of analyses to improve the result, which explains the smaller traces in their approach. All in all, we consider that our approach gives better insights to understand the need for some of the requirements of the program transformations and the class of considered programs. For instance, most of our requirements come from the need to remove programs positions from the traces, as shown in Section 4.
Finally, [37] considers the reversible language RFUN. Similarly to Janus, computations in RFUN are reversible without the need of a Landauer embedding. The paper also presents a transformation from a simple (irreversible) functional language, FUN, to RFUN, in order to highlight how irreversibilities are handled in RFUN. The transformation has some similarities with both the approach of [24] and our improved transformation in Section 5.3; on the other hand, though, [37] also applies the Bennett trick [6] in order to avoid some unnecessary information.
8 Discussion and Future Work
In this paper, we have introduced a reversible extension of term rewriting. In order to keep our approach as general as possible, we have initially considered DCTRSs as input systems, and proved the soundness and reversibility of our extension of rewriting. Then, in order to introduce a reversibilization transformation for these systems, we have also presented a transformation from DCTRSs to pure constructor systems (pcDCTRSs) which is correct for constructor reduction. A further improvement is presented for injective functions, which may have a significant impact in memory usage in some cases. Finally, we have successfully applied our approach in the context of bidirectional program transformation.
We have developed a prototype implementation of the reversibilization transformations introduced in Section 5. The tool can read an input TRS file (format .trs [1]) and then it applies in a sequential way the following transformations: flattening, simplification of constructor conditions, injectivization, and inversion. The tool prints out the CTRSs obtained at each transformation step. It is publicly available through a web interface from http://kaz.dsic.upv.es/rev-rewriting.html, where we have included a number of examples to easily test the tool.
As for future work, we plan to investigate new methods to further reduce the size of the traces. In particular, we find it interesting to define a reachability analysis for DCTRSs. A reachability analysis for CTRSs without extra-variables (1-CTRSs) can be found in [12], but the extension to deal with extra-variables in DCTRSs (since a DCTRS is a particular case of 3-CTRS) seems challenging. Furthermore, as mentioned in the paper, a completion procedure to add default cases to some functions (as suggested in Section 5.1) may help to broaden the applicability of the technique and avoid the restriction to constructor reduction. Finally, our injectivization and inversion transformations are correct w.r.t. innermost reduction. Extending our results to a lazy strategy is also an interesting topic for further research.
Acknowledgements
We thank the anonymous reviewers for their useful comments and suggestions to improve this paper.
References
-
[1]
Annual international termination competition.
Available from URL:
http://www.termination-portal.org/wiki/Termination_Competition. - [2] S. Abramsky. A structural approach to reversible computation. Theoretical Computer Science, 347(3):441–464, 2005.
- [3] J. M. Almendros-Jiménez and G. Vidal. Automatic partial inversion of inductively sequential functions. In Z. Horváth, V. Zsók, and A. Butterfield, editors, Implementation and Application of Functional Languages, 18th International Symposium (IFL 2006), Revised Selected Papers, volume 4449 of Lecture Notes in Computer Science, pages 253–270. Springer, 2007.
- [4] F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
- [5] F. Bancilhon and N. Spyratos. Update semantics of relational views. ACM Transactions on Database Systems, 6(4):557–575, 1981.
- [6] C. H. Bennett. Logical reversibility of computation. IBM Journal of Research and Development, 17:525–532, 1973.
- [7] C. H. Bennett. Notes on the history of reversible computation. IBM Journal of Research and Development, 44(1):270–278, 2000.
- [8] J. Bergstra and J. Klop. Conditional Rewrite Rules: confluence and termination. Journal of Computer and System Sciences, 32:323–362, 1986.
- [9] P. Crescenzi and C. H. Papadimitriou. Reversible simulation of space-bounded computations. Theoretical Computer Science, 143(1):159–165, 1995.
- [10] K. Czarnecki, J. N. Foster, Z. Hu, R. Lämmel, A. Schürr, and J. F. Terwilliger. Bidirectional transformations: A cross-discipline perspective. In R. F. Paige, editor, Proc. of the 2nd Int’l Conf. on Theory and Practice of Model Transformations (ICMT 2009), volume 5563 of Lecture Notes in Computer Science, pages 260–283. Springer, 2009.
- [11] A. Di Pierro, C. Hankin, and H. Wiklicky. Reversible combinatory logic. Mathematical Structures in Computer Science, 16(4):621–637, 2006.
- [12] G. Feuillade and T. Genet. Reachability in Conditional Term Rewriting Systems. Electronic Notes in Theoretical Computer Science, 86(1):133–146, 2003.
- [13] J. N. Foster, M. B. Greenwald, J. T. Moore, B. C. Pierce, and A. Schmitt. Combinators for bidirectional tree transformations: A linguistic approach to the view-update problem. ACM Transactions on Programming Languages and Systems, 29(3):17, 2007.
- [14] M. P. Frank. Introduction to reversible computing: motivation, progress, and challenges. In N. Bagherzadeh, M. Valero, and A. Ramírez, editors, Proceedings of the Second Conference on Computing Frontiers, pages 385–390. ACM, 2005.
- [15] T. Genet. Decidable Approximations of Sets of Descendants and Sets of Normal Forms. In T. Nipkow, editor, Proc. of the 9th International Conference on Rewriting Techniques and Applications (RTA’98), volume 1379 of Lecture Notes in Computer Science, pages 151–165. Springer, 1998.
- [16] T. Genet and Y. Salmon. Reachability Analysis of Innermost Rewriting. In M. Fernández, editor, Proc. of the 26th International Conference on Rewriting Techniques and Applications (RTA’15), volume 36 of LIPIcs, pages 177–193. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015.
- [17] E. Giachino, I. Lanese, and C. A. Mezzina. Causal-consistent reversible debugging. In S. Gnesi and A. Rensink, editors, Proc. of the 17th International Conference on Fundamental Approaches to Software Engineering (FASE 2014), volume 8411 of Lecture Notes in Computer Science, pages 370–384. Springer, 2014.
- [18] N. Hirokawa and G. Moser. Automated Complexity Analysis Based on the Dependency Pair Method. In A. Armando, P. Baumgartner, and G. Dowek, editors, Proc. of IJCAR 2008, volume 5195 of Lecture Notes in Computer Science, pages 364–379. Springer, 2008.
- [19] L. Huelsbergen. A logically reversible evaluator for the call-by-name lambda calculus. In T. Toffoli and M. Biafore, editors, Proc. of PhysComp96, pages 159–167. New England Complex Systems Institute, 1996.
- [20] COST Action IC1405 on Reversible Computation - extending horizons of computing. URL: http://revcomp.eu/.
- [21] W. E. Kluge. A reversible SE(M)CD machine. In P. W. M. Koopman and C. Clack, editors, Proc. of the 11th International Workshop on the Implementation of Functional Languages, IFL’99. Selected Papers, volume 1868 of Lecture Notes in Computer Science, pages 95–113. Springer, 2000.
- [22] R. Landauer. Irreversibility and heat generation in the computing process. IBM Journal of Research and Development, 5:183–191, 1961.
- [23] C. Lutz and H. Derby. Janus: A time-reversible language, 1986. A letter to R. Landauer. Available from URL http://tetsuo.jp/ref/janus.pdf.
- [24] K. Matsuda, Z. Hu, K. Nakano, M. Hamana, and M. Takeichi. Bidirectionalization transformation based on automatic derivation of view complement functions. In R. Hinze and N. Ramsey, editors, Proc. of the 12th ACM SIGPLAN International Conference on Functional Programming, ICFP 2007, pages 47–58. ACM, 2007.
- [25] K. Matsuda, Z. Hu, K. Nakano, M. Hamana, and M. Takeichi. Bidirectionalizing programs with duplication through complementary function derivation. Computer Software, 26(2):56–75, 2009. In Japanese.
- [26] A. Middeldorp and E. Hamoen. Completeness results for basic narrowing. Applicable Algebra in Engineering, Communication and Computing, 5:213–253, 1994.
- [27] K. Morita. Reversible simulation of one-dimensional irreversible cellular automata. Theoretical Computer Science, 148(1):157–163, 1995.
- [28] K. Morita. Computation in reversible cellular automata. International Journal of General Systems, 41(6):569–581, 2012.
- [29] S. Mu, Z. Hu, and M. Takeichi. An injective language for reversible computation. In D. Kozen and C. Shankland, editors, Proc. of the 7th International Conference on Mathematics of Program Construction (MPC 2004), volume 3125 of Lecture Notes in Computer Science, pages 289–313. Springer, 2004.
- [30] M. Nagashima, M. Sakai, and T. Sakabe. Determinization of conditional term rewriting systems. Theoretical Computer Science, 464:72–89, 2012.
- [31] N. Nishida, A. Palacios, and G. Vidal. Reversible term rewriting. In D. Kesner and B. Pientka, editors, Proc. of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD’16), volume 52 of LIPIcs, pages 28:1–28:18. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016.
- [32] N. Nishida, M. Sakai, and T. Sakabe. Soundness of unravelings for conditional term rewriting systems via ultra-properties related to linearity. Logical Methods in Computer Science, 8(3-4):1–49, Aug. 2012.
- [33] N. Nishida and G. Vidal. Program inversion for tail recursive functions. In M. Schmidt-Schauß, editor, Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011), volume 10 of LIPIcs, pages 283–298. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2011.
- [34] M. Schordan, D. R. Jefferson, P. D. B. Jr., T. Oppelstrup, and D. J. Quinlan. Reverse code generation for parallel discrete event simulation. In J. Krivine and J. Stefani, editors, Proc. of the 7th International Conference on Reversible Computation (RC 2015), volume 9138 of Lecture Notes in Computer Science, pages 95–110. Springer, 2015.
- [35] B. Stoddart, R. Lynas, and F. Zeyda. A virtual machine for supporting reversible probabilistic guarded command languages. Electronic Notes in Theoretical Computer Science, 253(6):33–56, 2010.
- [36] Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003.
- [37] M. K. Thomsen and H. B. Axelsen. Interpretation and programming of the reversible functional language RFUN. In R. Lämmel, editor, Proc. of the 27th Symposium on the Implementation and Application of Functional Programming Languages (IFL’15), pages 8:1–8:13. ACM, 2015.
- [38] T. Toffoli. Computation and construction universality of reversible cellular automata. Journal of Computer and System Sciences, 15(2):213–231, 1977.
- [39] T. Yamakami. One-way reversible and quantum finite automata with advice. Information and Computation, 239:122–148, 2014.
- [40] T. Yokoyama. Reversible computation and reversible programming languages. Electronic Notes in Theoretical Computer Science, 253(6):71–81, 2010.
- [41] T. Yokoyama, H. Axelsen, and R. Glück. Fundamentals of reversible flowchart languages. Theoretical Computer Science, 611:87–115, 2016.
- [42] T. Yokoyama, H. B. Axelsen, and R. Glück. Reversible flowchart languages and the structured reversible program theorem. In Proc. of the 35th International Colloquium on Automata, Languages and Programming (ICALP 2008), volume 5126 of Lecture Notes in Computer Science, pages 258–270. Springer, 2008.
- [43] T. Yokoyama and R. Glück. A reversible programming language and its invertible self-interpreter. In G. Ramalingam and E. Visser, editors, Proc. of the 2007 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation (PEPM 2007), pages 144–153. ACM, 2007.
- [44] P. Zuliani. Logical reversibility. IBM Journal of Research and Development, 45(6):807–818, 2001.